A propositional Boolean formula consists of Boolean variables connected by logical operators. Example operators include logical and (), logical or (), and logical negation  Given such a formula, the Boolean Satisfiability (SAT) problem asks the question whether there exists an assignment for the variables such that the formula evaluates to true. If there exists such an assignment, the formula is said to be satisfiable. If no such assignment exists, the formula is said to be unsatisfiable. For example, formula  y is satisfiable with satisfying assignment x=false and y=true, while formula  x  y is unsatisfiable.
The determination of satisfiability for arbitrary formulae—that is, the SAT problem—is known to be NP-Complete. NP-Complete is a complexity class of problems generally not believed to be solvable in polynomial time. Still, there exist many techniques to solve SAT problems generated from real world applications efficiently in practice. Because of this, SAT solver is widely used in many applications and is considered to be one of the most important tools for logic reasoning.
A Quantified Boolean Formula (QBF) is a generalized form of a Boolean formula that contains quantifiers. Quantifiers are of two types: universal or existential. As defined, universal quantifier ∀x f(x) means f(true)  f(false). Thus, for any assignment (true or false) of variable x, f(x) has to evaluate to true to make ∀x f(x) evaluates to true. The existential quantifier ∃x f(x) means f(true)  f(false). Thus, to make ∃x f(x) true, for at least one assignment (true or false) of variable x, f(x) has to be true.
Given a QBF where all of its variables are quantified, the question of determining whether the formula evaluates to true or false is called a QBF satisfiability problem, sometimes called QBF problem. In a QBF formula, a variable is called a universal variable if it is universally quantified; it is called an existential variable if it is existentially quantified.
An example of a QBF formula is the following formula (1):∀x∃y  (1)The formula means that, for all values of x (“∀x”), there exists a value for y (“∃y”) which satisfies the propositional Boolean formula “ ”. In the example of formula (1), the quantifiers are at the beginning of the formula, this is called prenex form. All QBF formulas can be transformed into prenex form. In this form, the quantified variables are grouped into different groups. In this example, the innermost group is existential with a single variable y, and outermost group is a universal group containing the variable x.
Because a propositional Boolean formula is considered satisfied if at least one assignment of values to variables leads to an evaluation of the formula as true, SAT can be regarded as a special case of QBF problem, with all the variables being existential. In the general case, QBF problem is known to belong to a class of problems called P-Space Complete, which is believed to be more difficult than SAT.
The most widely used technique for solving SAT is the well known Davis-Logemann-Loveland (DLL) search based technique. To use this technique, the Boolean formula is transformed into Conjunctive Normal Form (CNF) by introducing auxiliary variables. The resulting CNF formula is equi-satisfiable to the original formula, means that if the CNF formula is satisfiable, then the original formula is as well, and if the CNF formula is not satisfiable, then the original formula is not.
A CNF formula is a logical and () of one or more clauses, each clause is a logical or () of one or more literals. A literal is either the positive or the negative form of a variable, e.g. “x” or  where x is a variable. Because it is the logical and of the clauses, to satisfy a CNF formula, each clause must be satisfied individually. Additionally, for a certain clause, if all but one of its literals has been assigned the value false, then the remaining literal must be assigned the value true in order to satisfy this clause. Such a clause is called a unit clause. If all literals in a clause are assigned value false, then the clause evaluates to false and the formula cannot be satisfied under current assignment. Such a clause is called a conflict clause.
The DLL algorithm is a search based algorithm that finds a satisfying solution by branching, deducing and backtracking. The branch process chooses a variable and assigns it with a value (true or false). The deduction process then looks at the clauses and detects any clause that is a unit clause or a conflict clause, given the values that have been assigned to the variables. If there is a unit clause, it assigns the free variable in the unit clause a value in order to make it satisfy the clause. If there is a conflict clause, the solver backtracks to undo some of the branching decisions, and try a different search space (i.e. resolve the current conflict). If no unit clauses or conflict clauses are found, the branch process is invoked and another variable is assigned a value.
Smart decision heuristics have been proposed to improve the deduction process. Techniques have been developed to perform deduction efficiently. Processes such as learning in the conflict analysis and non-chronological backtracking procedures have been developed to prevent the same conflicts from occurring in the future search. These techniques make SAT solver very efficient in practice.
The DLL technique is described in the following pseudo-code in Table 1:
TABLE 1DLL Technique for SAT Solver PseudocodeDLL Technique for SAT ( ){ while(true) {  decide_next_branch( );//Branching  while (true)  {   status = deduce( );//Deducing   if (status == conflict)   {    blevel = analyze_conflicts( );// Resolve Conflict    if (blevel < 0)     return UNSATISFIABLE;    else     back_track(blevel);//Backtracking   }   else if (status == satisfied)    return SATISFIABLE;//Found Satisfying Assignment   else    break;  } }}
This code describes a loop which sets an assignment (decide_next_branch) and attempts to determine if there's a conflict (deduce). If there is a conflict (“status==conflict”) then the conflict is analyzed to see how many levels of branching should be backtracked (“backtrack (blevel))”) or to see if there is no option for satisfiability (“if (blevel<0) return UNSATISFIABLE”). If deduce has found an assignment which makes the formula satisfied, this is returned (“return SATISFIABLE”).
The DLL technique has also been adapted by many researchers to solve the QBF problem as well. The DLL technique for solving QBF can be described in pseudo code as follows in Table 2:
TABLE 2DLL Technique for QBF Solver PseudocodeDLL Technique for QBF ( ){ while(true) {  decide_next_branch( );//Branching  while (true)  {   status = deduce( );//Deducing   if (status == conflict)   {    blevel = analyze_conflicts( );//analyze how to//resolve conflict    if (blevel < 0)     return UNSATISFIABLE;    else     back_track(blevel);  //Backtracking   }   else if (status == satisfied)   {    blevel = analyze_satisfaction( );//how to resolve//satisfaction    if (blevel < 0)     return SATIAFIABLE;    else     back_track(blevel);//Backtracking   }   else    break;  } }}
As can be seen, this DLL technique for QBF is very similar to DLL technique for SAT, except that in QBF, when a satisfied status is resulted from deduction, the solver needs to resolve the satisfaction and backtrack. The reason for this is because of the universally quantified variables. Since universal variables demand that the formula to be true regardless of whether the variable is assigned true or false, therefore, the solver needs to try both values for a universal variable before it can declare the formula to be satisfiable. In QBF solvers, a conflict clause does not necessarily have all its literals evaluate to false. Instead, there are well known rules to determine if a clause is conflicting or not. In the following, when in QBF context, we use these special rules to determine if a clause is conflict or if a cube is satisfied.
Different ways have been proposed to optimize the technique described above for QBF. Similar efficient deduction techniques and learning techniques as SAT solving have been proposed for QBF. These proposed techniques require that the input formula be in CNF. If the original formula is not in CNF, the solvers introduce new variables to make an equi-satisfiable CNF, and existentially quantify the new variables at the innermost quantification level.
Such a formulation has a serious shortcoming. In a CNF formula, it is easy to detect conflicts. As long as there is a single conflicting clause (in the SAT case, a clause with all literals evaluate to false, in QBF case, some similar rule concerning literals within a clause), the formula is conflicting. Efficient techniques have been proposed to perform this detection quickly. This is one of the reasons why the DLL technique is so successful determining SAT.
However, it is very difficult to detect satisfaction. To detect satisfaction in a CNF formula, the solver must make sure that each clause in the formula has at least one literal evaluate to true. This is an expensive operation. For DLL SAT solver, this shortcoming is not a big problem because we need to detection satisfaction only once. If it is satisfied, the solving process is over. However, for QBF problem, the difficulty in detecting satisfaction is a more serious problem, because both satisfaction and conflict need to be detected in the searching process. The satisfaction part is much more expensive to detect due to the asymmetry resulting from the CNF formulation of the problem. Thus, the CNF formulation helps with the determination of SAT using DLL technique, but for QBF it is time- and resource-consuming.